/*
 * ClauseSet.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef CLAUSESET_HPP_
#define CLAUSESET_HPP_

#include <string>
#include <iostream>
#include <sstream>

#include <boost/unordered_set.hpp>

#include "bfr/Clause.hpp"

namespace bfr {

/**
 * A ClauseSet is a set of Clause objects. Again, we use pointers.
 *
 * This class can be used to represent DNFs / CNFs, depending
 * on the context this object is used in.
 *
 * We will make some assumptions about the form of ClauseSets.
 * We assume that the variables in the set are numbered from
 * 0 to \f$n-1\f$ where n is the number of variables in the set.
 * This must not be true but if you create an algorithm that does something
 * with a ClauseSet you should assume this.
 *
 * When the ClauseSet object gets deleted also all Clause objects in
 * it will be deleted, and so all the Literal objects in the Clauses.
 *
 * You may assume that the clause will not change after it has been added
 * to this clause set (for example if you put them into a hash map).
 *
 * The clauses are stored in a
 * <a href="http://www.boost.org/doc/libs/1_49_0/doc/html/boost/unordered_set.html">
 * boost::unordered_set</a>.
 */
class ClauseSet {

    private:
        /**
         * Type of the set holding the clauses.
         */
        typedef boost::unordered_set<const Clause*,
                    Clause::clause_hash_struct,
                    Clause::clause_equals_struct> hash_clause_set_t;

    public:
        /**
         * Iterator type for the objects in this set.
         */
        typedef hash_clause_set_t::const_iterator
                const_iterator;

        /**
         * Default constructor.
         */
        ClauseSet();

        /**
         * Constructor given an initial size.
         *
         * The initialSize is used to create a hash map
         * that is big enough to hold the number of elements
         * without expensive rehashing.
         *
         * Of course you can add more elements than initial size,
         * but then maybe some rehashing will bee done.
         *
         * Actually we create a hash set of size
         * \f$2 \cdot initialSize\f$.
         * I think this is too much... We can run some tests maybe.
         *
         * @param initialSize The size at the beginning.
         */
        explicit ClauseSet(size_t initialSize);

        /**
         * Destructor.
         */
        ~ClauseSet();

        /**
         * Check whether a Clause is contained in this set.
         *
         * @return <code>true</code> if the set contains the Clause.
         */
        inline bool contains(const Clause *clause) const;

        /**
         * Add a Clause to this set.
         *
         * If this method returns <code>false</code>
         * the clause object will not be deleted when this
         * set is deleted.
         *
         * @param clause The clause to add.
         *
         * @return <code>true</code> if the insertion took place.
         *
         * @see Clause#add
         */
        bool add(const Clause *clause);

        /**
         * Return an iterator to the beginning.
         *
         * @return An iterator to the beginning.
         */
        inline const_iterator begin() const;

        /**
         * Return an iterator to the end.
         *
         * @return An iterator to the end.
         */
        inline const_iterator end() const;

        /**
         * Return the size of this ClauseSet (number of Clauses in it).
         *
         * @return Number of Clauses in the ClauseSet.
         */
        inline size_t size() const;

        /**
         * Add a Clause to the ClauseSet, delete the object if insertion failed
         *
         * This method just calls the ordinary add() method. But if the method
         * returns <code>false</code> it will delete the Clause.
         *
         * @param clause The Clause to add.
         *
         * @return <code>true</code> if the Clause was added,
         * <code>false</code> otherwise.
         *
         * @see Clause#addSecure
         */
        bool addSecure(const Clause *clause);

        /**
         * Write a DIMACS representation of this set the a stream.
         *
         * The DIMACS file format is widely used to describe CNFs.
         * The problem type of the problem line is set to "cnf".
         *
         * For a description of the DIMACS format see
         * <a href="http://logic.pdmi.ras.ru/~basolver/dimacs.html">
         * here</a>.
         */
        void writeDIMACS(std::ostream &out) const;

        /**
         * Write the set to a stream.
         *
         * @return The input stream.
         */
        friend std::ostream& operator<<(std::ostream& os, const ClauseSet &cs) {
            os << '{';
            bool first = true;
            const_iterator e = cs.end();

            for(const_iterator it = cs.begin();
                    it != e;
                    it++) {
                if(first)
                    first = false;
                else
                    os << ", ";
                os << *(*it);
            }
            os << '}';
            return os;
        }

        /**
         * Return a string representation.
         *
         * @return Human readable string version.
         */
        std::string asString() const;

        /**
         * Compare two ClauseSets.
         *
         * Two clause sets are equal if they contain
         * exactly the same clauses.
         *
         * Again, this does not check for semantic
         * equivalence.
         *
         * @return <code>true</code> if the two ClauseSets
         * contain exactly the same Clauses.
         *
         * @see Clause#operator==
         */
        bool operator ==(const ClauseSet &other) const;

        /**
         * Compare to ClauseSets.
         *
         * Two clause sets are not equal if the operator ==
         * returns false.
         *
         * @see ClauseSet#operator==
         */
        bool operator !=(const ClauseSet &other) const;

        /**
         * Same as in Clause#getVariableCount, returns maximum over all
         * clauses.
         *
         * @return Maximum of all Clause#getVariableCount over all
         * clauses in the set.
         */
        inline size_t getMaxLiteralId() const;

    private:
        // the set that holds the clauses
        hash_clause_set_t clauses;
        // the current maxid
        size_t maxID;
};

// some inline methods

bool ClauseSet::contains(const Clause *clause) const {
    return clauses.count(clause);
}

ClauseSet::const_iterator ClauseSet::begin() const {
    return clauses.begin();
}

ClauseSet::const_iterator ClauseSet::end() const {
    return clauses.end();
}

size_t ClauseSet::size() const {
    return clauses.size();
}

size_t ClauseSet::getMaxLiteralId() const {
    return maxID;
}

} // namespace bfr

#endif  // CLAUSESET_HPP_
